\begin{tabbing}
$\forall$\=$p$:FinProbSpace, $f$:($\mathbb{N}\rightarrow\mathbb{N}$), $X$:($n$:$\mathbb{N}\rightarrow$RandomVariable($p$;$f$($n$))), $N$:$\mathbb{N}$, $Z$:RandomVariable($p$;$N$),\+
\\[0ex]$n$:$\mathbb{N}$.
\-\\[0ex]($\forall$$i$:\{0..$n$$^{-}$\}. $f$($i$) $<$ $N$)
\\[0ex]$\Rightarrow$ ($\forall$$i$:\{0..($n$ {-} 1)$^{-}$\}. rv{-}disjoint($p$;$N$;$X$($i$);$Z$))
\\[0ex]$\Rightarrow$ ($\forall$$k$:\{0..$n$$^{-}$\}. rv{-}disjoint($p$;$N$;rv{-}partial{-}sum($k$;$i$.$X$($i$));$Z$))
\end{tabbing}